package ch.epfl.lara.pm.analyze;
/**
 * A trait that defines operators to compose and build boolean formulae
 */
trait Proposition {

  def dnf[T](basecase: T,or: (T,T) => T, and: (T,T) => T)(atoms: List[List[T]]): T  = 
    (atoms.:\ (basecase)) {
      (atom,acc) => or(conjunction(and)(atom),acc)
    }
  
  def cnf[T](basecase: T,and: (T,T) => T, or: (T,T) => T)(atoms: List[List[T]]): T  = 
    (atoms.:\ (basecase)) {
      (atom,acc) => and(conjunction(or)(atom),acc)
    }

  def disjunction[T](or: (T,T) => T)(propositions: List[T]): T = makeAtom(or)(propositions)
  
  def conjunction[T](and: (T,T) => T)(propositions: List[T]): T = makeAtom(and)(propositions)
  
  
  def makeAtom[T](operator: (T,T) => T)(propositions: List[T]): T = 
    propositions.reduceRight[T]((a,b) => operator(a,b))
    
  def disjointUnion[T](neg: T => T, and: (T,T) => T) (setA: T, setB: T): T = neg(and(setA,setB))
  
  def disjoint[S,T](disjointUnionFunction: (S,S) => T) (sets: List[S]): List[T] = {
    val length = sets.length
    for(i<-List.range(0,length); 
        j<-List.range(i+1,length)) yield disjointUnionFunction(sets(i),sets(j))
  }
}
